(**
   A functional parsing library, adapted from both the HOL Light and
Isabelle parsing libraries.
  I ascribe less general types to these functions to make them more
readable.  If one needs these to apply to more general lists where
the input is not a list of strings, one may either make this
a functor over the type token, or give them the most general
types by simply removing this interface file.  
 *)

(* -------------------------------------------------------------------------- *)
(*  Lexical analysis                                                          *)
(* -------------------------------------------------------------------------- *)

(**
   Some vanilla lexical analysis functions.
 *)
val matches : string -> string -> bool
val space : string -> bool
val punctuation : string -> bool
val symbolic : string -> bool
val numeric : string -> bool
val alphanumeric : string -> bool
val alpha : string -> bool
val lexwhile : (string -> bool) -> string list -> string * string list
val lex : string list -> string list
val lex_float : string list -> string list

(* -------------------------------------------------------------------------- *)
(*  Parsing                                                                   *)
(* -------------------------------------------------------------------------- *)

type token = string

type 'a parser = token list -> 'a * token list

exception Parse of string

(** Assert the contents of next token *)
val a : token -> token parser

(** Accept the next token, as a string *)
val next : string parser 

(** apply a function to the first element of a pair *)
val papply : ('a -> 'b) -> 'a * 'c list -> 'b * 'c list

(** Checks to see if the next token is a particular token *)
val nextin : token list -> token -> bool

(** After parsing an opening bracket, parse the following tokens with the supplied 
    parser, looking for the supplied closing bracket.  Return the resulting parser. *)
val parse_bracketed : 'a parser -> token -> 'a parser

(** 
    parse_ginfix opsym opupdate sof subparser inp
    parses inp with subparser, looks ahead to see if the next token is opsym.
    If it is not, then it applies sof to the output.  If it is not,
    it recursively parses, using opupdate to modify sof.  
 *)
val parse_ginfix : token -> (('a -> 'b) -> 'a -> 'a -> 'b) -> ('a -> 'b) -> 'a parser -> 'b parser

(**
   parses a left infix operator
 *)
val parse_left_infix : token -> ('a * 'a -> 'a) -> 'a parser -> 'a parser
(** 
   parses a right infix operator    
*) 
val parse_right_infix : token -> ('a * 'a -> 'a) -> 'a parser -> 'a parser

(** 
    parse_list sep p input
    uses p to parse a list (seperated by sep) in input
 *)
val parse_list : token -> 'a parser -> 'a list parser

(** make_parser p input 
    parses input with p, makes sure it consumes all the input, 
    and returns the parsed result
*)
val make_parser : 'a parser -> string -> 'a

(** make_parser lexer p input 
    parses input, (lexed with lex) with p, makes sure it consumes all the input, 
    and returns the parsed result
*)
val make_gen_parser : (string list -> token list) -> 'a parser -> string -> 'a

(**
   p1 || p2 
   tries p1 then p2 with backtracking upon failure
 *)
val ( || ) : 'a parser -> 'a parser -> 'a parser

(**
   (p1 ++ p2) input
   parses input with p1, then the remaining input with p2, returning the
   pair of the parsed asts
 *)
val ( ++ ) : 'a parser -> 'b parser -> ('a * 'b) parser


(**
   many p input
   runs p on the input as many times as it can, returning the list
 *)
val many : 'a parser -> 'a list parser

(** (p >> f) input 
     parses input with p and applies f to the resulting ast *)
val ( >> ) : 'a parser -> ('a -> 'b) -> ('b) parser

(** 
  fix msg p input 
  parses input with p, failing with message msg upon failure
 *)
val fix : string -> ('a -> 'b) -> 'a -> 'b


(**
   listof parser sep_parser err_msg input
   parses a list using parser, with sep_parser to parse
   the separater.  This is a generalization of parse_list for
   complicated seperators.  It fails with err_msg if parser
   fails after a successful sep_parser.
 *)
val listof : 'a parser -> 'b parser -> string -> 'a list parser

(** 
    The "do nothing" parser, returns the empty list
 *)
val nothing : 'a list parser

(**
   try to parse, returning an option
*) 
val maybe : 'a parser -> 'a option parser

(**
   make sure predicate applies to next element of input,
   and parse it.
 *)
val some : (token -> bool) -> token parser

(**
   Use 'many', but fail if you don't get at least n successes
 *)
val atleast : int -> 'a parser -> 'a list parser

(**
   try to parse a list, (using 'listof') but if you fail just do nothing.
 *)
val elistof : 'a parser -> 'b parser -> string -> 'a list parser

(**
   parse a list, folding (right) cons_fun over the result
 *)
val rightbin : 'a parser -> 'b parser -> ('a -> 'a -> 'a) -> string -> 'a parser

(**
   parse a list, folding cons_fun (left) over the result
 *)
val leftbin : 'a parser -> 'b parser -> ('a -> 'a -> 'a) -> string -> 'a parser

val parse_int : int parser
(* val parse_num : Num.num parser *)

(** 
   parses *non-negative* floats
 *)
val parse_float : float parser


module Ops : 
sig
  val ( || ) : 'a parser -> 'a parser -> 'a parser
  val ( ++ ) : 'a parser -> 'b parser -> ('a * 'b) parser
  val ( >> ) : 'a parser -> ('a -> 'b) -> ('b) parser
end
